I was curious to know between the 2 solution above ,
does the 2nd Solution ( using Go-To Non - Consecutive Repetition ) offer a better
Simulation Efficiency over the Consecutive Repetition ?
Is there any other alternative which would be more efficient ?
In reply to hisingh: readStart |=> readID[ *1: ] ##1 `readData[ *1: ] ##1readEnd ; readStart |=> readID[ ->1 ] ##1 readData[ → 1 ] ##1 `readEnd[ → 1 ] ;
They are not the same. The goto a[->1] is equivalent to (!a[*0:$] ##1 a)
a |=> b[ *1:$ ] ##1 c[ *1:$ ] ##1 d; in a state machine seems to
define the transitions between states, or basically a reiteration of the RTL code.
This is NOT how you verify a FSM. Aside from mathematical analysis for lockups and unreachable states, You can use SVA to verify the requirements. Here is an example from my SVA book in verifying 2 different FSM architectures for a traffic light controller, with specs defined in the book. Below is the module for the SVA to be bound to the RTL. Could have also use a SV checker instead of a module. As you can see from the SVA, I address the requirements and not the transitions between states.
`define true 1
`ifndef MULTIPLE_FILE_COMPILE
typedef enum {OFF, RED, YELLOW, GREEN, PRE_GREEN} lights_t;
`endif
module tlight_props
(
input lights_t ns_light, // North/South light status, Main road
input lights_t ew_light, // East/West light status
input ew_sensor, // East/West sensor for new car
input emgcy_sensor, // emergency sensor
input reset_n, // synchronous reset
input clk, // master clock
// internal states:
input [1:0] ns_green_timer
);
timeunit 1ns;
timeprecision 1ns;
parameter FAIL = 1'b0;
// sequence defintion
sequence qEmgcy;
@ (posedge clk) emgcy_sensor;
endsequence : qEmgcy
// **************************************************
// Safety property
property Never_NS_EW_ALL_GREEN;
disable iff (!reset_n)
not (ns_light==GREEN && ew_light==GREEN);
endproperty : Never_NS_EW_ALL_GREEN
Never_NS_EW_ALL_GREEN_1 : assert property(@ (posedge clk) Never_NS_EW_ALL_GREEN);
// **************************************************
// State of lights at reset
property nsLightAtReset;
// disable iff (!reset_n)
reset_n==1'b0 |=> ns_light==OFF;
endproperty : nsLightAtReset
nsLightAtReset_1 : assert property(@ (posedge clk) nsLightAtReset);
//
property ewLightAtReset;
// disable iff (!reset_n)
reset_n==1'b0 |=> ew_light==OFF;
endproperty : ewLightAtReset
ewLightAtReset_1 : assert property(@ (posedge clk) ewLightAtReset);
// **************************************************
// State of lights during emergency
// Lights switch from GREEN to YELLOW to RED
property NsLightsWhenEmergency;
disable iff (!reset_n)
emgcy_sensor |=> `true[*2] ##1 ns_light==RED;
endproperty : NsLightsWhenEmergency
NsLightsWhenEmergency_1 : assert property(@ (posedge clk) NsLightsWhenEmergency);
//
property EwLightsWhenEmergency;
disable iff (!reset_n)
emgcy_sensor |=> `true[*2] ##1 ew_light==RED;
endproperty : EwLightsWhenEmergency
EwLightsWhenEmergency_1 : assert property(@ (posedge clk) EwLightsWhenEmergency);
// **************************************************
// Safety, GREEN to RED is illegal. Need YELLOW
property NsNeverFromGreenToRed;
disable iff (!reset_n)
not(ns_light==GREEN ##1 ns_light==RED);
endproperty : NsNeverFromGreenToRed
NsNeverFromGreenToRed_1 : assert property(@ (posedge clk) NsNeverFromGreenToRed);
//
property EwNeverFromGreenToRed;
disable iff (!reset_n)
not(ew_light==GREEN ##1 ew_light==RED);
endproperty : EwNeverFromGreenToRed
EwNeverFromGreenToRed_1 : assert property(@ (posedge clk) EwNeverFromGreenToRed);
// **************************************************
// The NorthSouth light is the main street light.
// If ns is green and no emergency or ew sensor, then next cycle is also GREEN
property NsGreenNext;
(ns_light==GREEN) && ($past(emgcy_sensor)==1'b0 && reset_n==1'b1
// && ew_green_req == 1'b0) |=> ns_light==GREEN;
) |=> ns_light==GREEN;
endproperty : NsGreenNext
NsGreenNext_1: assert property (@ (posedge clk) NsGreenNext);
// **************************************************
// East-West light to RED errata 3/23/05
// // property EwLightToRed;
// // disable iff (!reset_n || emgcy_sensor)
// // (ew_green_timer==2'b11) |=>
// // `true ##1 ew_light==RED; // abort emgcy_sensor==1'b1);
// // endproperty : EwLightToRed
// // EwLightToRed_1 : assert property (EwLightToRed);
// GREEN-YELLOW at the smae time
property NeverGreenYellow;
not ((ew_light==GREEN && ns_light==YELLOW) ||
(ns_light==GREEN && ew_light==YELLOW));
endproperty : NeverGreenYellow
NeverGreenYellow_1: assert property (@ (posedge clk) NeverGreenYellow);
// NEW PROPERTIES 09/10/09
// **************************************************
// The NorthSouth light is the main street light.
// It must remain GREEN for ns_green_timer == 3 before it can switch.
// Timer ns_green_timer will count to 3, and remain at 3 until light changes.
property NsGreenForMin3Ccyles;
@ (posedge clk) disable iff (!reset_n || emgcy_sensor)
$rose(ns_light==GREEN) && !$past(emgcy_sensor) |=>
ns_light==GREEN[*2]; // abort emgcy_sensor);
// ns_light==GREEN ##1 ns_light==GREEN; // abort emgcy_sensor);
endproperty : NsGreenForMin3Ccyles
NsGreenForMin3Ccyles_1 : assert property (NsGreenForMin3Ccyles);
// **************************************************
// East-West North-South Lights with East-West sensor
// If ew_sensor is activated (new car), then light will switch for the ew_light
// when minimum time for ns_light is satisfied. ew_green_timer will count to 3,
// at which time, the ns_green_timer will regain control of GREEN.
property EwNewSensorActivation;
@ (posedge clk) disable iff (!reset_n || emgcy_sensor)
( (ew_sensor==1'b1) && $rose(ns_green_timer==2'b11 )) && !$past(emgcy_sensor) && ns_light!= RED |=>
ns_light==YELLOW ##1 ew_light==GREEN;
endproperty : EwNewSensorActivation
EwNewSensorActivation_1 : assert property (EwNewSensorActivation);
// End of new properties 09/10/09
// assign ew_is_green = (ew_light==GREEN) ? 1'b1 : 1'b0;
// assign ns_is_green = (ns_light==GREEN) ? 1'b1 : 1'b0;
endmodule : tlight_props
bind trafficlight tlight_props tlight_props1 (.*);