A method for automatically generating requirements based test cases using equivalence class analysis, the method comprising: converting, by a textual converter unit, textual design requirements to sets of machine-readable version of design requirements, one or more textual design requirements including a time domain component; partitioning, by a requirement partition unit, the machine-readable design requirements into one or more sets of related design requirements, wherein related design requirements are those requirements that impact a same set of output variables; processing, by an equivalence class partition unit, the sets of related design requirements and input/output variables into a set of equivalence classes; analyzing, by an equivalence class analyzer unit, the set of equivalence classes: identifying, by a boundary class analyzer unit, boundaries of the equivalence classes, the boundaries including at least one of a behavior transition between adjacent equivalence classes and a time domain boundary within an equivalence class; applying equivalence class analysis to the time domain boundary to obtain a set of time domain test cases; optimizing and subsequently combining, using a satisfiability modulo theory solver, the time domain test cases to obtain a second set of test cases, the second set of test cases having a quantity less than the set of test cases before the optimizing and combining; and removing redundant clauses from the second set of test cases. converting, by a textual converter unit, textual design requirements to sets of machine-readable version of design requirements, one or more textual design requirements including a time domain component; partitioning, by a requirement partition unit, the machine-readable design requirements into one or more sets of related design requirements, wherein related design requirements are those requirements that impact a same set of output variables; processing, by an equivalence class partition unit, the sets of related design requirements and input/output variables into a set of equivalence classes; analyzing, by an equivalence class analyzer unit, the set of equivalence classes: identifying, by a boundary class analyzer unit, boundaries of the equivalence classes, the boundaries including at least one of a behavior transition between adjacent equivalence classes and a time domain boundary within an equivalence class; applying equivalence class analysis to the time domain boundary to obtain a set of time domain test cases; optimizing and subsequently combining, using a satisfiability modulo theory solver, the time domain test cases to obtain a second set of test cases, the second set of test cases having a quantity less than the set of test cases before the optimizing and combining; and removing redundant clauses from the second set of test cases. identifying, by a boundary class analyzer unit, boundaries of the equivalence classes, the boundaries including at least one of a behavior transition between adjacent equivalence classes and a time domain boundary within an equivalence class; applying equivalence class analysis to the time domain boundary to obtain a set of time domain test cases; optimizing and subsequently combining, using a satisfiability modulo theory solver, the time domain test cases to obtain a second set of test cases, the second set of test cases having a quantity less than the set of test cases before the optimizing and combining; and removing redundant clauses from the second set of test cases.