diff --git a/sv-parser-parser/src/declarations/assertion_declarations.rs b/sv-parser-parser/src/declarations/assertion_declarations.rs
index ebbb346..03331bb 100644
--- a/sv-parser-parser/src/declarations/assertion_declarations.rs
+++ b/sv-parser-parser/src/declarations/assertion_declarations.rs
@@ -307,6 +307,7 @@ pub(crate) fn property_spec(s: Span) -> IResult<Span, PropertySpec> {
 pub(crate) fn property_expr(s: Span) -> IResult<Span, PropertyExpr> {
     alt((
         alt((
+            property_expr_binary,
             property_expr_implication_overlapped,
             property_expr_implication_nonoverlapped,
             property_expr_followed_by_overlapped,
@@ -316,26 +317,18 @@ pub(crate) fn property_expr(s: Span) -> IResult<Span, PropertyExpr> {
             }),
             property_expr_strong,
             property_expr_weak,
-            property_expr_paren,
             property_expr_not,
-            property_expr_or,
-            property_expr_and,
+            property_expr_paren,
+        )),
+        alt((
             property_expr_if,
             property_expr_case,
             property_expr_nexttime,
             property_expr_s_nexttime,
-        )),
-        alt((
             property_expr_always,
             property_expr_s_always,
             property_expr_eventually,
             property_expr_s_eventually,
-            property_expr_until,
-            property_expr_s_until,
-            property_expr_until_with,
-            property_expr_s_until_with,
-            property_expr_implies,
-            property_expr_iff,
             property_expr_accept_on,
             property_expr_reject_on,
             property_expr_sync_accept_on,
@@ -373,7 +366,7 @@ pub(crate) fn property_expr_weak(s: Span) -> IResult<Span, PropertyExpr> {
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn property_expr_paren(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = paren(sequence_expr)(s)?;
+    let (s, a) = paren(property_expr)(s)?;
     Ok((
         s,
         PropertyExpr::Paren(Box::new(PropertyExprParen { nodes: (a,) })),
@@ -394,26 +387,22 @@ pub(crate) fn property_expr_not(s: Span) -> IResult<Span, PropertyExpr> {
 #[recursive_parser]
 #[tracable_parser]
 #[packrat_parser]
-pub(crate) fn property_expr_or(s: Span) -> IResult<Span, PropertyExpr> {
+pub(crate) fn property_expr_binary(s: Span) -> IResult<Span, PropertyExpr> {
     let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("or")(s)?;
+    let (s, b) = alt((
+        keyword("or"),
+        keyword("and"),
+        keyword("until_with"),
+        keyword("until"),
+        keyword("s_until_with"),
+        keyword("s_until"),
+        keyword("implies"),
+        keyword("iff"),
+    ))(s)?;
     let (s, c) = property_expr(s)?;
     Ok((
         s,
-        PropertyExpr::Or(Box::new(PropertyExprOr { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_and(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("and")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::And(Box::new(PropertyExprAnd { nodes: (a, b, c) })),
+        PropertyExpr::Binary(Box::new(PropertyExprBinary { nodes: (a, b, c) })),
     ))
 }
 
@@ -580,84 +569,6 @@ pub(crate) fn property_expr_s_eventually(s: Span) -> IResult<Span, PropertyExpr>
     ))
 }
 
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_until(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("until")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::Until(Box::new(PropertyExprUntil { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_s_until(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("s_until")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::SUntil(Box::new(PropertyExprSUntil { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_until_with(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("until_with")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::UntilWith(Box::new(PropertyExprUntilWith { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_s_until_with(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("s_until_with")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::SUntilWith(Box::new(PropertyExprSUntilWith { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_implies(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("implies")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::Implies(Box::new(PropertyExprImplies { nodes: (a, b, c) })),
-    ))
-}
-
-#[recursive_parser]
-#[tracable_parser]
-#[packrat_parser]
-pub(crate) fn property_expr_iff(s: Span) -> IResult<Span, PropertyExpr> {
-    let (s, a) = property_expr(s)?;
-    let (s, b) = keyword("iff")(s)?;
-    let (s, c) = property_expr(s)?;
-    Ok((
-        s,
-        PropertyExpr::Iff(Box::new(PropertyExprIff { nodes: (a, b, c) })),
-    ))
-}
-
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn property_expr_accept_on(s: Span) -> IResult<Span, PropertyExpr> {
@@ -852,15 +763,15 @@ pub(crate) fn sequence_expr(s: Span) -> IResult<Span, SequenceExpr> {
     alt((
         sequence_expr_cycle_delay_expr,
         sequence_expr_expr_cycle_delay_expr,
-        sequence_expr_expression,
-        sequence_expr_instance,
-        sequence_expr_paren,
-        sequence_expr_and,
-        sequence_expr_intersect,
-        sequence_expr_or,
-        sequence_expr_first_match,
         sequence_expr_throughout,
+        terminated(sequence_expr_expression, peek(not(symbol("(")))),
+        sequence_expr_instance,
+        sequence_expr_and,
+        sequence_expr_or,
+        sequence_expr_intersect,
         sequence_expr_within,
+        sequence_expr_paren,
+        sequence_expr_first_match,
         sequence_expr_clocking_event,
     ))(s)
 }
@@ -1155,12 +1066,12 @@ pub(crate) fn sequence_list_of_arguments_named(s: Span) -> IResult<Span, Sequenc
 #[packrat_parser]
 pub(crate) fn sequence_actual_arg(s: Span) -> IResult<Span, SequenceActualArg> {
     alt((
-        map(event_expression_sequence_actual_arg, |x| {
-            SequenceActualArg::EventExpression(Box::new(x))
-        }),
         map(sequence_expr, |x| {
             SequenceActualArg::SequenceExpr(Box::new(x))
         }),
+        map(event_expression_sequence_actual_arg, |x| {
+            SequenceActualArg::EventExpression(Box::new(x))
+        }),
     ))(s)
 }
 
diff --git a/sv-parser-parser/src/expressions/numbers.rs b/sv-parser-parser/src/expressions/numbers.rs
index 2236566..f7a3807 100644
--- a/sv-parser-parser/src/expressions/numbers.rs
+++ b/sv-parser-parser/src/expressions/numbers.rs
@@ -104,8 +104,18 @@ pub(crate) fn hex_number(s: Span) -> IResult<Span, HexNumber> {
 #[packrat_parser]
 pub(crate) fn sign(s: Span) -> IResult<Span, Sign> {
     alt((
-        map(symbol("+"), |x| Sign::Plus(Box::new(x))),
-        map(symbol("-"), |x| Sign::Minus(Box::new(x))),
+        map(
+            map(tag("+"), |x: Span| Symbol {
+                nodes: (into_locate(x), vec![]),
+            }),
+            |x| Sign::Plus(Box::new(x)),
+        ),
+        map(
+            map(tag("-"), |x: Span| Symbol {
+                nodes: (into_locate(x), vec![]),
+            }),
+            |x| Sign::Minus(Box::new(x)),
+        ),
     ))(s)
 }
 
@@ -146,8 +156,13 @@ pub(crate) fn real_number(s: Span) -> IResult<Span, RealNumber> {
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn real_number_floating(s: Span) -> IResult<Span, RealNumber> {
-    let (s, a) = unsigned_number(s)?;
-    let (s, b) = opt(pair(symbol("."), unsigned_number))(s)?;
+    let (s, a) = unsigned_number_without_ws(s)?;
+    let (s, b) = opt(pair(
+        map(tag("."), |x: Span| Symbol {
+            nodes: (into_locate(x), vec![]),
+        }),
+        unsigned_number_without_ws,
+    ))(s)?;
     let (s, c) = exp(s)?;
     let (s, d) = opt(sign)(s)?;
     let (s, e) = unsigned_number(s)?;
@@ -162,7 +177,7 @@ pub(crate) fn real_number_floating(s: Span) -> IResult<Span, RealNumber> {
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn fixed_point_number(s: Span) -> IResult<Span, FixedPointNumber> {
-    let (s, a) = unsigned_number(s)?;
+    let (s, a) = unsigned_number_without_ws(s)?;
     let (s, b) = map(tag("."), |x: Span| Symbol {
         nodes: (into_locate(x), vec![]),
     })(s)?;
@@ -173,10 +188,24 @@ pub(crate) fn fixed_point_number(s: Span) -> IResult<Span, FixedPointNumber> {
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn exp(s: Span) -> IResult<Span, Exp> {
-    let (s, a) = alt((symbol("e"), symbol("E")))(s)?;
+    let (s, a) = alt((
+        map(tag("e"), |x: Span| Symbol {
+            nodes: (into_locate(x), vec![]),
+        }),
+        map(tag("E"), |x: Span| Symbol {
+            nodes: (into_locate(x), vec![]),
+        }),
+    ))(s)?;
     Ok((s, Exp { nodes: (a,) }))
 }
 
+#[tracable_parser]
+#[packrat_parser]
+pub(crate) fn unsigned_number_without_ws(s: Span) -> IResult<Span, UnsignedNumber> {
+    let (s, a) = unsigned_number_impl(s)?;
+    Ok((s, UnsignedNumber { nodes: (a, vec![]) }))
+}
+
 #[tracable_parser]
 #[packrat_parser]
 pub(crate) fn unsigned_number(s: Span) -> IResult<Span, UnsignedNumber> {
diff --git a/sv-parser-parser/src/tests.rs b/sv-parser-parser/src/tests.rs
index b028de2..92dad83 100644
--- a/sv-parser-parser/src/tests.rs
+++ b/sv-parser-parser/src/tests.rs
@@ -7514,40 +7514,40 @@ mod spec {
                 end"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"a1: assert property (@clk $future_gclk(a || $rising_gclk(b));
-        //        sequence s;
-        //          bit v;
-        //          (a, v = a) ##1 (b == v)[->1];
-        //        endsequence : s
+        test!(
+            many1(module_item),
+            r##"a1: assert property (@clk $future_gclk(a || $rising_gclk(b)));
+                sequence s;
+                  bit v;
+                  (a, v = a) ##1 (b == v)[->1];
+                endsequence : s
 
-        //        // Illegal: a global clocking future sampled value function shall not
-        //        // be used in an assertion containing sequence match items
-        //        a2: assert property (@clk s |=> $future_gclk(c));"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"a1: assert property (@$global_clock $changing_gclk(sig)
-        //                                         |-> $falling_gclk(clk))
-        //        else $error(”sig is not stable”);"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"a2: assume property(@$global_clock
-        //                    $falling_gclk(clk) ##1 (!$falling_gclk(clk)[*1:$]) |->
-        //                                                          $steady_gclk(sig));"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"a3: assert property (@$global_clock disable iff (rst) $changing_gclk(sig)
-        //                                             |-> $falling_gclk(clk))
-        //        else $error(”sig is not stable”);"##,
-        //    Ok((_, _))
-        //);
+                // Illegal: a global clocking future sampled value function shall not
+                // be used in an assertion containing sequence match items
+                a2: assert property (@clk s |=> $future_gclk(c));"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"a1: assert property (@($global_clock) $changing_gclk(sig)
+                                                 |-> $falling_gclk(clk))
+                else $error("sig is not stable");"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"a2: assume property(@($global_clock)
+                            $falling_gclk(clk) ##1 (!$falling_gclk(clk)[*1:$]) |->
+                                                                  $steady_gclk(sig));"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"a3: assert property (@($global_clock) disable iff (rst) $changing_gclk(sig)
+                                                     |-> $falling_gclk(clk))
+                else $error("sig is not stable");"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"a4: assert property (##1 $stable_gclk(sig));
@@ -7565,25 +7565,25 @@ mod spec {
                 endsequence"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence t2;
-        //          (a ##[2:3] b) or (c ##[1:2] d);
-        //        endsequence
-        //        sequence ts2;
-        //          first_match(t2);
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence burst_rule1;
-        //          @(posedge mclk)
-        //            $fell(burst_mode) ##0
-        //            ((!burst_mode) throughout (##2 ((trdy==0)&&(irdy==0)) [*7]));
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"sequence t2;
+                  (a ##[2:3] b) or (c ##[1:2] d);
+                endsequence
+                sequence ts2;
+                  first_match(t2);
+                endsequence"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence burst_rule1;
+                  @(posedge mclk)
+                    $fell(burst_mode) ##0
+                    ((!burst_mode) throughout (##2 ((trdy==0)&&(irdy==0)) [*7]));
+                endsequence"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"sequence s;
@@ -7595,27 +7595,27 @@ mod spec {
                 endsequence"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence e1;
-        //          @(posedge sysclk) $rose(ready) ##1 proc1 ##1 proc2 ;
-        //        endsequence
-        //        sequence rule;
-        //          @(posedge sysclk) reset ##1 inst ##1 e1.triggered ##1 branch_back;
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence e2(a,b,c);
-        //          @(posedge sysclk) $rose(a) ##1 b ##1 c;
-        //        endsequence
-        //        sequence rule2;
-        //          @(posedge sysclk) reset ##1 inst ##1 e2(ready,proc1,proc2).triggered
-        //            ##1 branch_back;
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"sequence e1;
+                  @(posedge sysclk) $rose(ready) ##1 proc1 ##1 proc2 ;
+                endsequence
+                sequence rule;
+                  @(posedge sysclk) reset ##1 inst ##1 e1.triggered ##1 branch_back;
+                endsequence"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence e2(a,b,c);
+                  @(posedge sysclk) $rose(a) ##1 b ##1 c;
+                endsequence
+                sequence rule2;
+                  @(posedge sysclk) reset ##1 inst ##1 e2(ready,proc1,proc2).triggered
+                    ##1 branch_back;
+                endsequence"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"sequence e2_instantiated;
@@ -7645,13 +7645,14 @@ mod spec {
                 endsequence"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence s;
-        //          logic u, v = a, w = v || b;
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"sequence s;
+                  logic u, v = a, w = v || b;
+                  u;
+                endsequence"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property e;
@@ -7660,18 +7661,18 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence data_check;
-        //          int x;
-        //          a ##1 (!a, x = data_in) ##1 !b[*0:$] ##1 b && (data_out == x);
-        //        endsequence
-        //        property data_check_p
-        //          int x;
-        //          a ##1 (!a, x = data_in) |=> !b[*0:$] ##1 b && (data_out == x);
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"sequence data_check;
+                  int x;
+                  a ##1 (!a, x = data_in) ##1 !b[*0:$] ##1 b && (data_out == x);
+                endsequence
+                property data_check_p;
+                  int x;
+                  a ##1 (!a, x = data_in) |=> !b[*0:$] ##1 b && (data_out == x);
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"sequence rep_v;
@@ -7736,46 +7737,46 @@ mod spec {
                 endsequence"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence s4;
-        //          int x;
-        //          (a ##1 (b, x = data) ##1 c) or (d ##1 (e==x)); // illegal
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence s5;
-        //          int x,y;
-        //          ((a ##1 (b, x = data, y = data1) ##1 c)
-        //            or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2);
-        //          // illegal because y is not in the intersection
-        //        endsequence
-        //        sequence s6;
-        //          int x,y;
-        //          ((a ##1 (b, x = data, y = data1) ##1 c)
-        //            or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (x==data2);
-        //          // legal because x is in the intersection
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence s7;
-        //          int x,y;
-        //          ((a ##1 (b, x = data, y = data1) ##1 c)
-        //            and (d ##1 (`true, x = data) ##0 (e==x))) ##1 (x==data2);
-        //          // illegal because x is common to both threads
-        //        endsequence
-        //        sequence s8;
-        //          int x,y;
-        //          ((a ##1 (b, x = data, y = data1) ##1 c)
-        //            and (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2);
-        //          // legal because y is in the difference
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"sequence s4;
+                  int x;
+                  (a ##1 (b, x = data) ##1 c) or (d ##1 (e==x)); // illegal
+                endsequence"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence s5;
+                  int x,y;
+                  ((a ##1 (b, x = data, y = data1) ##1 c)
+                    or (d ##1 (true, x = data) ##0 (e==x))) ##1 (y==data2);
+                  // illegal because y is not in the intersection
+                endsequence
+                sequence s6;
+                  int x,y;
+                  ((a ##1 (b, x = data, y = data1) ##1 c)
+                    or (d ##1 (true, x = data) ##0 (e==x))) ##1 (x==data2);
+                  // legal because x is in the intersection
+                endsequence"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence s7;
+                  int x,y;
+                  ((a ##1 (b, x = data, y = data1) ##1 c)
+                    and (d ##1 (true, x = data) ##0 (e==x))) ##1 (x==data2);
+                  // illegal because x is common to both threads
+                endsequence
+                sequence s8;
+                  int x,y;
+                  ((a ##1 (b, x = data, y = data1) ##1 c)
+                    and (d ##1 (true, x = data) ##0 (e==x))) ##1 (y==data2);
+                  // legal because y is in the difference
+                endsequence"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"sequence s1;
@@ -7944,56 +7945,56 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property p1;
-        //          a until b;
-        //        endproperty
+        test!(
+            many1(module_item),
+            r##"property p1;
+                  a until b;
+                endproperty
 
-        //        property p2;
-        //          a s_until b;
-        //        endproperty
+                property p2;
+                  a s_until b;
+                endproperty
 
-        //        property p3;
-        //          a until_with b;
-        //        endproperty
+                property p3;
+                  a until_with b;
+                endproperty
 
-        //        property p4;
-        //          a s_until_with b;
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p1;
-        //          s_eventually a;
-        //        endproperty
+                property p4;
+                  a s_until_with b;
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p1;
+                  s_eventually a;
+                endproperty
 
-        //        property p2;
-        //          s_eventually always a;
-        //        endproperty
+                property p2;
+                  s_eventually always a;
+                endproperty
 
-        //        property p3;
-        //          always s_eventually a;
-        //        endproperty
+                property p3;
+                  always s_eventually a;
+                endproperty
 
-        //        property p4;
-        //          eventually [2:5] a;
-        //        endproperty
+                property p4;
+                  eventually [2:5] a;
+                endproperty
 
-        //        property p5;
-        //          s_eventually [2:5] a;
-        //        endproperty
+                property p5;
+                  s_eventually [2:5] a;
+                endproperty
 
-        //        property p6;
-        //          eventually [2:$] a; // Illegal
-        //        endproperty
+                //property p6;
+                //  eventually [2:$] a; // Illegal
+                //endproperty
 
-        //        property p7;
-        //          s_eventually [2:$] a;
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+                property p7;
+                  s_eventually [2:$] a;
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"assert property (@(clk) go ##1 get[*2] |-> reject_on(stop) put[->2]);"##,
@@ -8004,26 +8005,26 @@ mod spec {
             r##"assert property (@(clk) go ##1 get[*2] |-> sync_reject_on(stop) put[->2]);"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"assert property (@(clk) go ##1 get[*2] |-> !stop throughout put[->2]);"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p; (accept_on(a) p1) and (reject_on(b) p2); endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p; (accept_on(a) p1) or (reject_on(b) p2); endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p; not (accept_on(a) p1); endproperty"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"assert property (@(clk) go ##1 get[*2] |-> !stop throughout put[->2]);"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p; (accept_on(a) p1) and (reject_on(b) p2); endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p; (accept_on(a) p1) or (reject_on(b) p2); endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p; not (accept_on(a) p1); endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property p; accept_on(a) reject_on(b) p1; endproperty"##,
@@ -8042,13 +8043,13 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property prop_always(p);
-        //          p and (1'b1 |=> prop_always(p));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"property prop_always(p);
+                  p and (1'b1 |=> prop_always(p));
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property p1(s,p);
@@ -8056,13 +8057,13 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property prop_weak_until(p,q);
-        //          q or (p and (1'b1 |=> prop_weak_until(p,q)));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"property prop_weak_until(p,q);
+                  q or (p and (1'b1 |=> prop_weak_until(p,q)));
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property p2(s,p,q);
@@ -8070,35 +8071,35 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property check_phase1;
-        //          s1 |-> (phase1_prop and (1'b1 |=> check_phase2));
-        //        endproperty
-        //        property check_phase2;
-        //          s2 |-> (phase2_prop and (1'b1 |=> check_phase1));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property illegal_recursion_1(p);
-        //          not prop_always(not p);
-        //        endproperty
+        test!(
+            many1(module_item),
+            r##"property check_phase1;
+                  s1 |-> (phase1_prop and (1'b1 |=> check_phase2));
+                endproperty
+                property check_phase2;
+                  s2 |-> (phase2_prop and (1'b1 |=> check_phase1));
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property illegal_recursion_1(p);
+                  not prop_always(not p);
+                endproperty
 
-        //        property illegal_recursion_2(p);
-        //          p and (1'b1 |=> not illegal_recursion_2(p));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property illegal_recursion_3(p);
-        //          disable iff (b)
-        //          p and (1'b1 |=> illegal_recursion_3(p));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+                property illegal_recursion_2(p);
+                  p and (1'b1 |=> not illegal_recursion_2(p));
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property illegal_recursion_3(p);
+                  disable iff (b)
+                  p and (1'b1 |=> illegal_recursion_3(p));
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property legal_3(p);
@@ -8106,50 +8107,50 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property illegal_recursion_4(p);
-        //          p and (1'b1 |-> illegal_recursion_4(p));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property fibonacci1 (local input int a, b, n, int fib_sig);
-        //          (n > 0)
-        //          |->
-        //          (
-        //            (fib_sig == a)
-        //            and
-        //            (1'b1 |=> fibonacci1(b, a + b, n - 1, fib_sig))
-        //          );
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property fibonacci2 (int a, b, n, fib_sig);
-        //          (n > 0)
-        //          |->
-        //          (
-        //            (fib_sig == a)
-        //            and
-        //            (1'b1 |=> fibonacci2(b, a + b, n - 1, fib_sig))
-        //          );
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p3(p, bit b, abort);
-        //          (p and (1'b1 |=> p4(p, b, abort)));
-        //        endproperty
+        test!(
+            many1(module_item),
+            r##"property illegal_recursion_4(p);
+                  p and (1'b1 |-> illegal_recursion_4(p));
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property fibonacci1 (local input int a, b, n, int fib_sig);
+                  (n > 0)
+                  |->
+                  (
+                    (fib_sig == a)
+                    and
+                    (1'b1 |=> fibonacci1(b, a + b, n - 1, fib_sig))
+                  );
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property fibonacci2 (int a, b, n, fib_sig);
+                  (n > 0)
+                  |->
+                  (
+                    (fib_sig == a)
+                    and
+                    (1'b1 |=> fibonacci2(b, a + b, n - 1, fib_sig))
+                  );
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p3(p, bit b, abort);
+                  (p and (1'b1 |=> p4(p, b, abort)));
+                endproperty
 
-        //        property p4(p, bit b, abort);
-        //          accept_on(b) reject_on(abort) p3(p, b, abort);
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+                property p4(p, bit b, abort);
+                  accept_on(b) reject_on(abort) p3(p, b, abort);
+                endproperty"##,
+            Ok((_, _))
+        );
         //test!(
         //    many1(module_item),
         //    r##"property check_write;
@@ -8214,32 +8215,32 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property rule3;
-        //          @(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property rule4;
-        //          @(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property rule5;
-        //          @(posedge clk)
-        //          a ##1 (b || c)[->1] |->
-        //            if (b)
-        //              (##1 d |-> e)
-        //            else // c
-        //              f ;
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"property rule3;
+                  @(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property rule4;
+                  @(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property rule5;
+                  @(posedge clk)
+                  a ##1 (b || c)[->1] |->
+                    if (b)
+                      (##1 d |-> e)
+                    else // c
+                      f ;
+                endproperty"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"property rule6(x,y);
@@ -8307,61 +8308,61 @@ mod spec {
                 endproperty"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property mult_p8;
-        //          @(posedge clk) a ##1 b |->
-        //          if (c)
-        //            (1 |=> @(posedge clk1) d)
-        //          else
-        //            e ##1 @(posedge clk2) f ;
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence e1(a,b,c);
-        //          @(posedge clk) $rose(a) ##1 b ##1 c ;
-        //        endsequence
-        //        sequence e2;
-        //          @(posedge sysclk) reset ##1 inst ##1 e1(ready,proc1,proc2).matched [->1]
-        //            ##1 branch_back;
-        //        endsequence"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"sequence e1;
-        //          @(posedge sysclk) $rose(a) ##1 b ##1 c;
-        //        endsequence
+        test!(
+            many1(module_item),
+            r##"property mult_p8;
+                  @(posedge clk) a ##1 b |->
+                  if (c)
+                    (1 |=> @(posedge clk1) d)
+                  else
+                    e ##1 @(posedge clk2) f ;
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence e1(a,b,c);
+                  @(posedge clk) $rose(a) ##1 b ##1 c ;
+                endsequence
+                sequence e2;
+                  @(posedge sysclk) reset ##1 inst ##1 e1(ready,proc1,proc2).matched [->1]
+                    ##1 branch_back;
+                endsequence"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"sequence e1;
+                  @(posedge sysclk) $rose(a) ##1 b ##1 c;
+                endsequence
 
-        //        sequence e2;
-        //          @(posedge sysclk) reset ##1 inst ##1 e1.triggered ##1 branch_back;
-        //        endsequence
+                sequence e2;
+                  @(posedge sysclk) reset ##1 inst ##1 e1.triggered ##1 branch_back;
+                endsequence
 
-        //        sequence e3;
-        //          @(posedge clk) reset1 ##1 e1.matched ##1 branch_back1;
-        //        endsequence
+                sequence e3;
+                  @(posedge clk) reset1 ##1 e1.matched ##1 branch_back1;
+                endsequence
 
-        //        sequence e2_with_arg(sequence subseq);
-        //          @(posedge sysclk) reset ##1 inst ##1 subseq.triggered ##1 branch_back;
-        //        endsequence
+                sequence e2_with_arg(sequence subseq);
+                  @(posedge sysclk) reset ##1 inst ##1 subseq.triggered ##1 branch_back;
+                endsequence
 
-        //        sequence e4;
-        //          e2_with_arg(@(posedge sysclk) $rose(a) ##1 b ##1 c);
-        //        endsequence
+                sequence e4;
+                  e2_with_arg(@(posedge sysclk) $rose(a) ##1 b ##1 c);
+                endsequence
 
-        //        program check;
-        //          initial begin
-        //            wait (e1.triggered || e2.triggered);
-        //            if (e1.triggered)
-        //              $display("e1 passed");
-        //            if (e2.triggered)
-        //              $display("e2 passed");
-        //          end
-        //        endprogram"##,
-        //    Ok((_, _))
-        //);
+                program check;
+                  initial begin
+                    wait (e1.triggered || e2.triggered);
+                    if (e1.triggered)
+                      $display("e1 passed");
+                    if (e2.triggered)
+                      $display("e2 passed");
+                  end
+                endprogram"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"module mod_sva_checks;
@@ -8440,47 +8441,47 @@ mod spec {
                 endmodule : mod_sva_checks"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"property p;
-        //          logic v = e;
-        //          (@(posedge clk1) (a == v)[*1:$] |-> b)
-        //          and
-        //          (@(posedge clk2) c[*1:$] |-> d == v)
-        //          ;
-        //        endproperty
-        //        a1: assert property (@(posedge clk) f |=> p);"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property p;
-        //          logic v;
-        //          (@(posedge clk1) (1, v = e) ##0 (a == v)[*1:$] |-> b)
-        //          and
-        //          (@(posedge clk2) (1, v = e) ##0 c[*1:$] |-> d == v)
-        //          ;
-        //        endproperty"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property abc(a, b, c);
-        //          disable iff (a==2) @(posedge clk) not (b ##1 c);
-        //        endproperty
-        //        env_prop: assert property (abc(rst, in1, in2))
-        //          $display("env_prop passed."); else $display("env_prop failed.");"##,
-        //    Ok((_, _))
-        //);
-        //test!(
-        //    many1(module_item),
-        //    r##"property abc(a, b, c);
-        //          disable iff (c) @(posedge clk) a |=> b;
-        //        endproperty
-        //        env_prop:
-        //          assume property (abc(req, gnt, rst)) else $error(”Assumption failed.”);"##,
-        //    Ok((_, _))
-        //);
+        test!(
+            many1(module_item),
+            r##"property p;
+                  logic v = e;
+                  (@(posedge clk1) (a == v)[*1:$] |-> b)
+                  and
+                  (@(posedge clk2) c[*1:$] |-> d == v)
+                  ;
+                endproperty
+                a1: assert property (@(posedge clk) f |=> p);"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property p;
+                  logic v;
+                  (@(posedge clk1) (1, v = e) ##0 (a == v)[*1:$] |-> b)
+                  and
+                  (@(posedge clk2) (1, v = e) ##0 c[*1:$] |-> d == v)
+                  ;
+                endproperty"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property abc(a, b, c);
+                  disable iff (a==2) @(posedge clk) not (b ##1 c);
+                endproperty
+                env_prop: assert property (abc(rst, in1, in2))
+                  $display("env_prop passed."); else $display("env_prop failed.");"##,
+            Ok((_, _))
+        );
+        test!(
+            many1(module_item),
+            r##"property abc(a, b, c);
+                  disable iff (c) @(posedge clk) a |=> b;
+                endproperty
+                env_prop:
+                  assume property (abc(req, gnt, rst)) else $error("Assumption failed.");"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"a1:assume property ( @(posedge clk) req dist {0:=40, 1:=60} ) ;
@@ -8761,35 +8762,35 @@ mod spec {
                 end"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"module m(logic a, b, c, d, rst1, clk1, clk2);
-        //          logic rst;
+        test!(
+            many1(module_item),
+            r##"module m(logic a, b, c, d, rst1, clk1, clk2);
+                  logic rst;
 
-        //          default clocking @(negedge clk1); endclocking
-        //          default disable iff rst1;
+                  default clocking @(negedge clk1); endclocking
+                  default disable iff rst1;
 
-        //          property p_triggers(start_event, end_event, form, clk = $inferred_clock,
-        //                              rst = $inferred_disable);
-        //            @clk disable iff (rst)
-        //              (start_event ##0 end_event[->1]) |=> form;
-        //          endproperty
+                  property p_triggers(start_event, end_event, form, clk = $inferred_clock,
+                                      rst = $inferred_disable);
+                    @clk disable iff (rst)
+                      (start_event ##0 end_event[->1]) |=> form;
+                  endproperty
 
-        //          property p_multiclock(clkw, clkx = $inferred_clock, clky, w, x, y, z);
-        //            @clkw w ##1 @clkx x |=> @clky y ##1 z;
-        //          endproperty
+                  property p_multiclock(clkw, clkx = $inferred_clock, clky, w, x, y, z);
+                    @clkw w ##1 @clkx x |=> @clky y ##1 z;
+                  endproperty
 
-        //          a1: assert property (p_triggers(a, b, c));
-        //          a2: assert property (p_triggers(a, b, c, posedge clk1, 1'b0) );
+                  a1: assert property (p_triggers(a, b, c));
+                  a2: assert property (p_triggers(a, b, c, posedge clk1, 1'b0) );
 
-        //          always @(posedge clk2 or posedge rst) begin
-        //          end
+                  always @(posedge clk2 or posedge rst) begin
+                  end
 
-        //          a4: assert property(p_multiclock(negedge clk2, , posedge clk1,
-        //                              a, b, c, d) );
-        //        endmodule"##,
-        //    Ok((_, _))
-        //);
+                  a4: assert property(p_multiclock(negedge clk2, , posedge clk1,
+                                      a, b, c, d) );
+                endmodule"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"module m(logic a, b, c, d, rst1, clk1, clk2);
@@ -8918,116 +8919,116 @@ mod spec {
                 assert property (p4);"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"module examples_with_default (input logic a, b, c, clk);
-        //          property q1;
-        //            $rose(a) |-> ##[1:5] b;
-        //          endproperty
+        test!(
+            many1(module_item),
+            r##"module examples_with_default (input logic a, b, c, clk);
+                  property q1;
+                    $rose(a) |-> ##[1:5] b;
+                  endproperty
 
-        //          property q2;
-        //            @(posedge clk) q1;
-        //          endproperty
+                  property q2;
+                    @(posedge clk) q1;
+                  endproperty
 
-        //          default clocking posedge_clk @(posedge clk);
-        //            property q3;
-        //              $fell(c) |=> q1;
-        //              // legal: q1 has no clocking event
-        //            endproperty
+                  default clocking posedge_clk @(posedge clk);
+                    property q3;
+                      $fell(c) |=> q1;
+                      // legal: q1 has no clocking event
+                    endproperty
 
-        //            property q4;
-        //              $fell(c) |=> q2;
-        //              // legal: q2 has clocking event identical to that of
-        //              // the clocking block
-        //            endproperty
+                    property q4;
+                      $fell(c) |=> q2;
+                      // legal: q2 has clocking event identical to that of
+                      // the clocking block
+                    endproperty
 
-        //            sequence s1;
-        //              @(posedge clk) b[*3];
-        //              // illegal: explicit clocking event in clocking block
-        //            endsequence
-        //          endclocking
+                    sequence s1;
+                      @(posedge clk) b[*3];
+                      // illegal: explicit clocking event in clocking block
+                    endsequence
+                  endclocking
 
-        //          property q5;
-        //            @(negedge clk) b[*3] |=> !b;
-        //          endproperty
+                  property q5;
+                    @(negedge clk) b[*3] |=> !b;
+                  endproperty
 
-        //          always @(negedge clk)
-        //          begin
-        //            a1: assert property ($fell(c) |=> q1);
-        //              // legal: contextually inferred leading clocking event,
-        //              // @(negedge clk)
-        //            a2: assert property (posedge_clk.q4);
-        //              // legal: will be queued (pending) on negedge clk, then
-        //              // (if matured) checked at next posedge clk (see 16.14.6)
-        //            a3: assert property ($fell(c) |=> q2);
-        //              // illegal: multiclocked property with contextually
-        //              // inferred leading clocking event
-        //            a4: assert property (q5);
-        //              // legal: contextually inferred leading clocking event,
-        //              // @(negedge clk)
-        //          end
+                  always @(negedge clk)
+                  begin
+                    a1: assert property ($fell(c) |=> q1);
+                      // legal: contextually inferred leading clocking event,
+                      // @(negedge clk)
+                    a2: assert property (posedge_clk.q4);
+                      // legal: will be queued (pending) on negedge clk, then
+                      // (if matured) checked at next posedge clk (see 16.14.6)
+                    a3: assert property ($fell(c) |=> q2);
+                      // illegal: multiclocked property with contextually
+                      // inferred leading clocking event
+                    a4: assert property (q5);
+                      // legal: contextually inferred leading clocking event,
+                      // @(negedge clk)
+                  end
 
-        //          property q6;
-        //            q1 and q5;
-        //          endproperty
+                  property q6;
+                    q1 and q5;
+                  endproperty
 
-        //          a5: assert property (q6);
-        //            // illegal: default leading clocking event, @(posedge clk),
-        //            // but semantic leading clock is not unique
-        //          a6: assert property ($fell(c) |=> q6);
-        //            // legal: default leading clocking event, @(posedge clk),
-        //            // is the unique semantic leading clock
+                  a5: assert property (q6);
+                    // illegal: default leading clocking event, @(posedge clk),
+                    // but semantic leading clock is not unique
+                  a6: assert property ($fell(c) |=> q6);
+                    // legal: default leading clocking event, @(posedge clk),
+                    // is the unique semantic leading clock
 
-        //          sequence s2;
-        //            $rose(a) ##[1:5] b;
-        //          endsequence
+                  sequence s2;
+                    $rose(a) ##[1:5] b;
+                  endsequence
 
-        //          c1: cover property (s2);
-        //            // legal: default leading clocking event, @(posedge clk)
-        //          c2: cover property (@(negedge clk) s2);
-        //            // legal: explicit leading clocking event, @(negedge clk)
-        //        endmodule
+                  c1: cover property (s2);
+                    // legal: default leading clocking event, @(posedge clk)
+                  c2: cover property (@(negedge clk) s2);
+                    // legal: explicit leading clocking event, @(negedge clk)
+                endmodule
 
-        //        module examples_without_default (input logic a, b, c, clk);
-        //          property q1;
-        //            $rose(a) |-> ##[1:5] b;
-        //          endproperty
+                module examples_without_default (input logic a, b, c, clk);
+                  property q1;
+                    $rose(a) |-> ##[1:5] b;
+                  endproperty
 
-        //          property q5;
-        //            @(negedge clk) b[*3] |=> !b;
-        //          endproperty
+                  property q5;
+                    @(negedge clk) b[*3] |=> !b;
+                  endproperty
 
-        //          property q6;
-        //            q1 and q5;
-        //          endproperty
+                  property q6;
+                    q1 and q5;
+                  endproperty
 
-        //          a5: assert property (q6);
-        //            // illegal: no leading clocking event
-        //          a6: assert property ($fell(c) |=> q6);
-        //            // illegal: no leading clocking event
+                  a5: assert property (q6);
+                    // illegal: no leading clocking event
+                  a6: assert property ($fell(c) |=> q6);
+                    // illegal: no leading clocking event
 
-        //          sequence s2;
-        //            $rose(a) ##[1:5] b;
-        //          endsequence
+                  sequence s2;
+                    $rose(a) ##[1:5] b;
+                  endsequence
 
-        //          c1: cover property (s2);
-        //            // illegal: no leading clocking event
-        //          c2: cover property (@(negedge clk) s2);
-        //            // legal: explicit leading clocking event, @(negedge clk)
+                  c1: cover property (s2);
+                    // illegal: no leading clocking event
+                  c2: cover property (@(negedge clk) s2);
+                    // legal: explicit leading clocking event, @(negedge clk)
 
-        //          sequence s3;
-        //            @(negedge clk) s2;
-        //          endsequence
+                  sequence s3;
+                    @(negedge clk) s2;
+                  endsequence
 
-        //          c3: cover property (s3);
-        //            // legal: leading clocking event, @(negedge clk),
-        //            // determined from declaration of s3
-        //          c4: cover property (s3 ##1 b);
-        //            // illegal: no default, inferred, or explicit leading
-        //            // clocking event and maximal property is not an instance
-        //        endmodule"##,
-        //    Ok((_, _))
-        //);
+                  c3: cover property (s3);
+                    // legal: leading clocking event, @(negedge clk),
+                    // determined from declaration of s3
+                  c4: cover property (s3 ##1 b);
+                    // illegal: no default, inferred, or explicit leading
+                    // clocking event and maximal property is not an instance
+                endmodule"##,
+            Ok((_, _))
+        );
         //test!(
         //    many1(module_item),
         //    r##"wire clk1, clk2;
@@ -9051,20 +9052,20 @@ mod spec {
                 endprogram"##,
             Ok((_, _))
         );
-        //test!(
-        //    many1(module_item),
-        //    r##"integer data;
-        //        task automatic wait_for( integer value, output bit success );
-        //        expect( @(posedge clk) ##[1:10] data == value ) success = 1;
-        //          else success = 0;
-        //        endtask
+        test!(
+            many1(module_item),
+            r##"integer data;
+                task automatic wait_for( integer value, output bit success );
+                expect( @(posedge clk) ##[1:10] data == value ) success = 1;
+                  else success = 0;
+                endtask
 
-        //        initial begin
-        //          bit ok;
-        //          wait_for( 23, ok ); // wait for the value 23
-        //        end"##,
-        //    Ok((_, _))
-        //);
+                initial begin
+                  bit ok;
+                  wait_for( 23, ok ); // wait for the value 23
+                end"##,
+            Ok((_, _))
+        );
         test!(
             many1(module_item),
             r##"module A;
@@ -15583,7 +15584,7 @@ mod spec {
 fn debug() {
     test!(
         many1(module_item),
-        r##"sequence legal_loc_var_formal ( local logic b = b_d, d = d_d); g ##1 h; endsequence"##,
+        r##"property p; (accept_on(a) p1) and (reject_on(b) p2); endproperty"##,
         Ok((_, _))
     );
 }
diff --git a/sv-parser-syntaxtree/src/declarations/assertion_declarations.rs b/sv-parser-syntaxtree/src/declarations/assertion_declarations.rs
index 2f19ba1..ab990d1 100644
--- a/sv-parser-syntaxtree/src/declarations/assertion_declarations.rs
+++ b/sv-parser-syntaxtree/src/declarations/assertion_declarations.rs
@@ -163,8 +163,7 @@ pub enum PropertyExpr {
     Weak(Box<PropertyExprWeak>),
     Paren(Box<PropertyExprParen>),
     Not(Box<PropertyExprNot>),
-    Or(Box<PropertyExprOr>),
-    And(Box<PropertyExprAnd>),
+    Binary(Box<PropertyExprBinary>),
     ImplicationOverlapped(Box<PropertyExprImplicationOverlapped>),
     ImplicationNonoverlapped(Box<PropertyExprImplicationNonoverlapped>),
     If(Box<PropertyExprIf>),
@@ -177,12 +176,6 @@ pub enum PropertyExpr {
     SAlways(Box<PropertyExprSAlways>),
     Eventually(Box<PropertyExprEventually>),
     SEventually(Box<PropertyExprSEventually>),
-    Until(Box<PropertyExprUntil>),
-    SUntil(Box<PropertyExprSUntil>),
-    UntilWith(Box<PropertyExprUntilWith>),
-    SUntilWith(Box<PropertyExprSUntilWith>),
-    Implies(Box<PropertyExprImplies>),
-    Iff(Box<PropertyExprIff>),
     AcceptOn(Box<PropertyExprAcceptOn>),
     RejectOn(Box<PropertyExprRejectOn>),
     SyncAcceptOn(Box<PropertyExprSyncAcceptOn>),
@@ -203,7 +196,7 @@ pub struct PropertyExprWeak {
 
 #[derive(Clone, Debug, Node)]
 pub struct PropertyExprParen {
-    pub nodes: (Paren<SequenceExpr>,),
+    pub nodes: (Paren<PropertyExpr>,),
 }
 
 #[derive(Clone, Debug, Node)]
@@ -212,12 +205,7 @@ pub struct PropertyExprNot {
 }
 
 #[derive(Clone, Debug, Node)]
-pub struct PropertyExprOr {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprAnd {
+pub struct PropertyExprBinary {
     pub nodes: (PropertyExpr, Keyword, PropertyExpr),
 }
 
@@ -304,36 +292,6 @@ pub struct PropertyExprSEventually {
     ),
 }
 
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprUntil {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprSUntil {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprUntilWith {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprSUntilWith {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprImplies {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
-#[derive(Clone, Debug, Node)]
-pub struct PropertyExprIff {
-    pub nodes: (PropertyExpr, Keyword, PropertyExpr),
-}
-
 #[derive(Clone, Debug, Node)]
 pub struct PropertyExprAcceptOn {
     pub nodes: (Keyword, Paren<ExpressionOrDist>, PropertyExpr),